Nuprl Lemma : mlnk_wf2
11,40
postcript
pdf
the_es
:ES,
m
:Msg. mlnk(
m
)
IdLnk
latex
Definitions
x
:
A
.
B
(
x
)
,
Msg
,
t
T
,
es-M(
es
)
,
t
.1
,
t
.2
,
ES
Lemmas
mlnk
wf
,
Msg
wf
,
event
system
wf
origin
the_es:ES, m:Msg. mlnk(m) 
IdLnk the_es:ES, m:Msg. mlnk(m) IdLnk x:A. B(x) T